A:Type, I:MaInterface(A), l:IdLnk, tg:Id, nmr:Namer(2;[tg; lname(l)] @ ma-interface-tags(I)).
Normal(A,I)
 gluable(I;l;tg)
 gluable2(A;I;l;tg)
 (k:Knd.
 (k  fpf-domain((mapl(i.if i = source(l)
 then ma-interface-conds(I;i)
 else es-in-port-conds(A;(link nmr(0) from i to source(l));nmr(1))
 fi ;remove-repeats(IdDeq;ma-interface-locs(I))))))
  (((mapl(i.if i = source(l)
  ((then ma-interface-conds(I;i)
  ((else es-in-port-conds(A;(link nmr(0) from i to source(l));nmr(1))
  ((fi ;remove-repeats(IdDeq;ma-interface-locs(I))))(k).1)
  & ((k = rcv(l,tg))))) 

latex

Definitions

x:A. B(x), P  Q, A, t  T, , A  B, False, P & Q, {i..j}, i  j < k, if b then t else f fi , tt, ff, , x. t(x), SQType(T), {T}, , State(ds), Top, f(x)?z, x  dom(f), deq-member(eq;x;L), reduce(f;k;as), Y, t.1, a:A fp B(a), (x  l), Knd, A c B, x:A. B(x), ma-interface-conds(I;i), f(x), t.2, S  T, es-in-port-conds(A;l;tg), x : v, P  Q, Namer(n;Id_list), , Unit, P  Q, x(s), P  Q, (xL.P(x)), Normal(A,I), Normal(T), Normal(ds), fpf-domain(f), gluable(I;l;tg), , a = b

Lemmas

gluable2 wf, gluable wf, ma-interface-normal wf, Namer wf, le wf, append wf, lname wf, ma-interface-tags wf, Id wf, IdLnk wf, ma-interface wf, ma-interface-loc wf, lsrc wf, bool wf, eqtt to assert, ma-interface-ds wf, assert-ma-interface-loc, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-empty wf, member-remove-repeats, Id sq, ma-interface-conds wf3, l member wf, remove-repeats wf, id-deq wf, ma-interface-locs wf, es-in-port-conds wf, mk lnk wf, subtype-fpf2, decl-state wf, top wf, subtype rel product, subtype rel function, subtype rel dep function, fpf-cap wf, subtype rel self, subtype-fpf-cap-top, fpf-empty-sub, eq id wf, assert-eq-id, not functionality wrt iff, fpf-domain wf, fpf-join-list wf, Knd wf, mapl wf, nat wf, length wf1, select wf, ma-interface-conds wf, fpf-trivial-subtype-top, fpf wf, member-fpf-domain, fpf-join-list-ap, pi1 wf, member-mapl, fpf-dom wf, fpf-ap wf, assert-deq-member, ma-interface-dom wf, hasloc wf, deq-member wf, bor wf, eq knd wf, rcv wf, bfalse wf, fpf-join-list-domain, bool cases, bool sq, Knd sq, member singleton, rcv one one, member append, cons member